(set-logic QF_UFC)
(set-info :status sat)
(declare-sort S0 0)
(declare-const S0-0 S0)
(assert (_ fmf.card S0 1))
(assert (_ fmf.card S0 4))
(check-sat)
